recognizer(es;i;ds;x;k;T;test)
== (@i(x:) & (state@i r State(ds)) & (kindtype(i;k) r T))
== c (e@i.
== c (((x after e))
== c ( (e':E. ((e' loc e & kind(e') = k) c ((test((state when e'),val(e'))))))
== c & x initially@i = ff)
recognizer(es;i;ds;x;k;T;test)
== (es-dtype(es;i;x;) & (es-state(es;i) r State(ds)) & (es-kindtype(es;i;k) r T))
== c (alle-at(es;i;e.(es-after(es; x; e))
== c (e':es-E(es)
== c (((es-le(es;e';e) & es-kind(es; e') = k Knd)
== c (c ((test(es-state-when(es;e'),es-val(es; e')))))))
== c & es-initially(es;i;x) = ff )